$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$). $f$ $\in$ $a$:\{$a$:$A$$\mid$ ($a$ $\in$ fpf{-}domain($f$))\}  fp$\rightarrow$ $B$($a$)